Verification of hybrid automata diagnosability by abstraction,” Automatic Control

Abstract—A notion of diagnosability for hybrid systems is defined, which generalizes the common notion of observability. We propose an abstraction procedure to translate a hybrid au-tomaton into a timed automaton, in order to verify observability and diagnosability properties. We introduce a procedure to check diagnosability, and show that for the system class of our abstrac-tion (namely for a subclass of timed automata: the durational graphs) the verification problem belongs to the complexity class P. We apply our procedure to an electromagnetic valve system for camless engines. Index Terms—Abstraction, automatic verification, diagnos-ability, hybrid systems, observability, timed automata. I